Nuprl Lemma : qless_functionality_wrt_implies_1
11,40
postcript
pdf
a
,
b
,
c
,
d
:
. (
b
a
)
c
d
{
b
<
c
a
<
d
}
latex
Definitions
t
T
,
{
T
}
,
P
Q
,
x
:
A
.
B
(
x
)
,
a
b
,
Lemmas
rationals
wf
,
qge
wf
,
qle
wf
,
qless
wf
,
qless
transitivity
2
qorder
,
qless
transitivity
1
qorder
origin
a, b, c, d:
. (b 
a) 
c 
d {b < c a < d} a, b, c, d:. (b a) c d {b < c a < d} 
T Qx:A. B(x) b